Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    app(app(append,nil),l)  → l
2:    app(app(append,app(app(cons,h),t)),l)  → app(app(cons,h),app(app(append,t),l))
3:    app(app(map,f),nil)  → nil
4:    app(app(map,f),app(app(cons,h),t))  → app(app(cons,app(f,h)),app(app(map,f),t))
5:    app(app(append,app(app(append,l1),l2)),l3)  → app(app(append,l1),app(app(append,l2),l3))
6:    app(app(map,f),app(app(append,l1),l2))  → app(app(append,app(app(map,f),l1)),app(app(map,f),l2))
There are 14 dependency pairs:
7:    APP(app(append,app(app(cons,h),t)),l)  → APP(app(cons,h),app(app(append,t),l))
8:    APP(app(append,app(app(cons,h),t)),l)  → APP(app(append,t),l)
9:    APP(app(append,app(app(cons,h),t)),l)  → APP(append,t)
10:    APP(app(map,f),app(app(cons,h),t))  → APP(app(cons,app(f,h)),app(app(map,f),t))
11:    APP(app(map,f),app(app(cons,h),t))  → APP(cons,app(f,h))
12:    APP(app(map,f),app(app(cons,h),t))  → APP(f,h)
13:    APP(app(map,f),app(app(cons,h),t))  → APP(app(map,f),t)
14:    APP(app(append,app(app(append,l1),l2)),l3)  → APP(app(append,l1),app(app(append,l2),l3))
15:    APP(app(append,app(app(append,l1),l2)),l3)  → APP(app(append,l2),l3)
16:    APP(app(append,app(app(append,l1),l2)),l3)  → APP(append,l2)
17:    APP(app(map,f),app(app(append,l1),l2))  → APP(app(append,app(app(map,f),l1)),app(app(map,f),l2))
18:    APP(app(map,f),app(app(append,l1),l2))  → APP(append,app(app(map,f),l1))
19:    APP(app(map,f),app(app(append,l1),l2))  → APP(app(map,f),l1)
20:    APP(app(map,f),app(app(append,l1),l2))  → APP(app(map,f),l2)
The approximated dependency graph contains one SCC: {7,8,10,12-15,17,19,20}.
Tyrolean Termination Tool  (0.09 seconds)   ---  May 3, 2006